We show that context semantics can be fruitfully applied to the quantitativeanalysis of proof normalization in linear logic. In particular, contextsemantics lets us define the weight of a proof-net as a measure of its inherentcomplexity: it is both an upper bound to normalization time (modulo apolynomial overhead, independently on the reduction strategy) and a lower boundto the number of steps to normal form (for certain reduction strategies).Weights are then exploited in proving strong soundness theorems for varioussubsystems of linear logic, namely elementary linear logic, soft linear logicand light linear logic.
展开▼
